M.pre(a,s,v) == P != 1of(2of(2of(2of(M))))(a)  P(s,v) 

latex

---

clarification:

M.pre(a,s,v) == fpf-val(IdDeq; 1of(2of(2of(2of(M)))); a; a,P.(P(s,v))) 

latex

Definitions	2of(t), 1of(t), IdDeq, z != f(x)  P(a;z)
FDL editor aliases	ma-pre